Issue2408-error.agda:15,8-9
Set (lsuc (l a)) != Set₁
when checking that the expression F has type A → X
